sync spec & code by arnaucube · Pull Request #107 · 0xPARC/pod2

arnaucube · 2025-03-03T21:34:58Z

resolves #103

arnaucube · 2025-03-03T21:38:01Z

book/src/operations.md

+<span style="color:red">WIP, the following ones were appearing at the docs table but not at the implementation ([src/middleware/operation.rs](https://github.com/0xPARC/pod2/blob/main/src/middleware/operation.rs#L20)):</span><br>
+<span style="color:red">TODO rm?</span>
+| Code | Identifier            | Args                | Condition                                                                                                             | Output                                                         |
+|------|-----------------------|---------------------|-----------------------------------------------------------------------------------------------------------------------|----------------------------------------------------------------|
 | 3    | `SymmetricEq`         | `s`                 | `s = Equal(ak1, ak2)`                                                                                                 | `Eq(ak2, ak1)`                                                 |
-| 4    | `TransitiveEq`        | `s1`, `s2`          | `s1 = Equal(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak2 = ak3`                                                           | `Eq(ak1, ak4)`                                                 |
-| 5    | `EntryNEq`            | `s1`, `s2`          | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 != value2`                                          | `NEq(ak1, ak2)`                                                |
 | 6    | `SymmetricNEq`        | `s`                 | `s = NotEqual(ak1, ak2)`                                                                                              | `NEq(ak2, ak1)`                                                |
-| 7    | `GtToNEq`             | `s`                 | `s = Gt(ak1, ak2)`                                                                                                    | `NEq(ak1, ak2)`                                                |
-| 8    | `LEqToNEq`            | `s`                 | `s = LEq(ak1, ak2)`                                                                                                   | `NEq(ak1, ak2)`                                                |
-| 9    | `EntryGt`             | `s1`, `s2`          | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 > value2`                                           | `Gt(ak1, ak2)`                                                 |
+| 16   | `RenameSintains`      | `s1`, `s2`          | `s1 = Sintains(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak1 = ak3`                                                        | `Sintains(ak4, ak2)`                                           |
+| 7    | `TransitiveEq`        | `s1`, `s2`          | `s1 = Equal(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak2 = ak3`                                                           | `Eq(ak1, ak4)`                                                 |
+| 6    | `LEqToNEq`            | `s`                 | `s = LEq(ak1, ak2)`                                                                                                   | `NEq(ak1, ak2)`                                                |


@ax0 @tideofwords , question: the table from lines 8 to 25 contains the same ops that are implemented at https://github.com/0xPARC/pod2/blob/main/src/middleware/operation.rs#L20 ; the table from lines 31 to 39 contains the ops that were at the table previous to this commit, but that don't appear at the rust impl. Should those ops be added to the implementation? or we should remove them from the spec?

After seeing #108 , thought about keeping the ones that appear in the 2nd table, with a comment remarking that those are not yet implemented. The changes can be seen at the commit fac9b7a .

Yes, this sounds good to me. I think we'll have to refine the list of operations anyway...

arnaucube · 2025-03-03T21:41:01Z

book/src/operations.md

 | 0    | `None`                |                     |                                                                                                                       | `None`                                                         |
 | 1    | `NewEntry`[^newentry] | `(key, value)`      |                                                                                                                       | `ValueOf(ak, value)`, where `ak` has key `key` and origin ID 1 |
-| 2    | `EntryEq`             | `s1`, `s2`          | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 = value2`                                           | `Eq(ak1, ak2)`                                                 |
+| 2    | `CopyStatement`       | `s`                 |                                                                                                                       |                                                                |
+| 3    | `EntryEq`             | `s1`, `s2`          | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 = value2`                                           | `Eq(ak1, ak2)`                                                 |
+| 4    | `EntryNEq`            | `s1`, `s2`          | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 != value2`                                          | `NEq(ak1, ak2)`                                                |
+| 5    | `EntryGt`             | `s1`, `s2`          | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 > value2`                                           | `Gt(ak1, ak2)`                                                 |
+| 6    | `EntryLEq`            | `s1`, `s2`          | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 <= value2`                                          | `LEq(ak1, ak2)`                                                |
+| 7    | `TransitiveEq`        | `s1`, `s2`          | `s1 = Equal(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak2 = ak3`                                                           | `Eq(ak1, ak4)`                                                 |
+| 8    | `GtToNEq`             | `s`                 | `s = Gt(ak1, ak2)`                                                                                                    | `NEq(ak1, ak2)`                                                |
+| 9    | `LtToNEq`             | `s`                 | `s = Lt(ak1, ak2)`                                                                                                    | `NEq(ak1, ak2)`                                                |
+| 10   | `EntryContains`       | `s1`, `s2`, `proof` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `merkle_includes(value1, value2, proof) = true`             | `Contains(ak1, ak2)`                                           |
+| 11   | `EntrySintains`       | `s1`, `s2`, `proof` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `merkle_excludes(value1, value2, proof) = true`             | `Sintains(ak1, ak2)`                                           |
+| 12   | `RenameContains`      | `s1`, `s2`          | `s1 = Contains(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak1 = ak3`                                                        | `Contains(ak4, ak2)`                                           |
+| 13   | `SumOf`               | `s1`, `s2`, `s3`    | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `s3 = ValueOf(ak3, value3)`, `value1 = value2 + value3`     | `SumOf(ak1, ak2, ak3)`                                         |
+| 14   | `ProductOf`           | `s1`, `s2`, `s3`    | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `s3 = ValueOf(ak3, value3)`, `value1 = value2 * value3`     | `ProductOf(ak1, ak2, ak3)`                                     |
+| 15   | `MaxOf`               | `s1`, `s2`, `s3`    | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `s3 = ValueOf(ak3, value3)`, `value1 = max(value2, value3)` | `MaxOf(ak1, ak2, ak3)`                                         |


(this table is updated to match the same enumeration as in https://github.com/0xPARC/pod2/blob/main/src/middleware/operation.rs#L20 )

arnaucube · 2025-03-03T21:49:33Z

book/src/statements.md

+| 4    | `Gt`          | `ak1`, `ak2`        | `value_of(ak1) > value_of(ak2)`                                   |
+| 5    | `LEq`         | `ak1`, `ak2`        | `value_of(ak1) <= value_of(ak2)`                                  |
+| 6    | `Contains`    | `ak1`, `ak2`        | `(key_of(ak2), value_of(ak2)) ∈ value_of(ak1)` (Merkle inclusion) |
+| 7    | `NotContains` | `ak1`, `ak2`        | `(key_of(ak2), value_of(ak2)) ∉ value_of(ak1)` (Merkle exclusion) |


did this change to make it match the implementation naming, but later realized that other sections of the spec use Sintains. Maybe we should stick to either Sintains or NotContains everywhere (code & spec).

Apparently Sintains has fallen out of favour, so we'll have to go with NotContains.

well in this specific line I changed it to NotContains but because is what I saw on other parts of the code, but later saw other sections of the spec that still use Sintains and left those with that. So even after this current PR we'll keep having both Sintains and NotContains at different places.
I think it's not a deal breaker for now, so not 'urgent' to fix, but something to have in mind and maybe over the next days we can agree on one of them.

arnaucube · 2025-03-04T17:50:26Z

book/src/merkletree.md

@@ -145,39 +145,48 @@ For the current use cases, we don't need to prove that the key exists but the va

 ```rust
 impl MerkleTree {


(the changes in this file are just to update the merkletree.md#Interface to match the rust implementation interface)

ax0

LGTM!

ax0 · 2025-03-05T10:20:58Z

book/src/statements.md

+| 4    | `Gt`          | `ak1`, `ak2`        | `value_of(ak1) > value_of(ak2)`                                   |
+| 5    | `LEq`         | `ak1`, `ak2`        | `value_of(ak1) <= value_of(ak2)`                                  |
+| 6    | `Contains`    | `ak1`, `ak2`        | `(key_of(ak2), value_of(ak2)) ∈ value_of(ak1)` (Merkle inclusion) |
+| 7    | `NotContains` | `ak1`, `ak2`        | `(key_of(ak2), value_of(ak2)) ∉ value_of(ak1)` (Merkle exclusion) |


Apparently Sintains has fallen out of favour, so we'll have to go with NotContains.

arnaucube added this to the Milestone 2 milestone Mar 3, 2025

arnaucube commented Mar 3, 2025

View reviewed changes

arnaucube force-pushed the sync-spec-and-code branch 2 times, most recently from 65564ab to 8387f8b Compare March 3, 2025 21:46

arnaucube commented Mar 3, 2025

View reviewed changes

sync spec & code

2245185

arnaucube force-pushed the sync-spec-and-code branch from 8387f8b to 2245185 Compare March 3, 2025 23:20

move primitives (merkletree) into the backend

7c933e8

arnaucube force-pushed the sync-spec-and-code branch from 66696cd to 7c933e8 Compare March 4, 2025 13:30

comment on the ops spec and link to issue #108

fac9b7a

arnaucube force-pushed the sync-spec-and-code branch from 7f37322 to fac9b7a Compare March 4, 2025 17:48

arnaucube marked this pull request as ready for review March 4, 2025 17:49

arnaucube requested review from ax0 and tideofwords March 4, 2025 17:49

arnaucube commented Mar 4, 2025

View reviewed changes

typo

4f7a8ed

arnaucube force-pushed the sync-spec-and-code branch from 1c5dccd to 4f7a8ed Compare March 4, 2025 17:53

ax0 approved these changes Mar 5, 2025

View reviewed changes

fix github-ci mdbook-publish pages

7aaf9df

tideofwords merged commit 02ec7c3 into main Mar 5, 2025
4 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

sync spec & code#107

sync spec & code#107
tideofwords merged 5 commits intomainfrom
sync-spec-and-code

arnaucube commented Mar 3, 2025 •

edited

Loading

Uh oh!

arnaucube Mar 3, 2025

Uh oh!

arnaucube Mar 4, 2025

Uh oh!

tideofwords Mar 5, 2025

Uh oh!

arnaucube Mar 3, 2025

Uh oh!

arnaucube Mar 3, 2025 •

edited

Loading

Uh oh!

ax0 Mar 5, 2025

Uh oh!

arnaucube Mar 5, 2025

Uh oh!

arnaucube Mar 4, 2025

Uh oh!

ax0 left a comment

Uh oh!

ax0 Mar 5, 2025

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

		@@ -145,39 +145,48 @@ For the current use cases, we don't need to prove that the key exists but the va

		```rust
		impl MerkleTree {

Conversation

arnaucube commented Mar 3, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

arnaucube Mar 3, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ax0 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

arnaucube commented Mar 3, 2025 •

edited

Loading

arnaucube Mar 3, 2025 •

edited

Loading